es:ES{i}, e, e':E, x:Id. e leaks x to e'  Prop{i'} 

latex

Definitions	x:A. B(x), t  T, Prop, e leaks x to e', x:A. B(x), P & Q, A & B, P  Q
Lemmas	not wf, es-atom wf, es-loc wf, inheres wf, es-state-without wf, es-state-when-without wf, atom-free-es-state-without, es-rcv-atom wf, assert wf, es-isrcv wf, es-E wf, es-sender wf, es-valtype wf, es-val wf, atom-free-es-valtype, Id wf, event system wf